Problem:
 *(i(x),x) -> 1()
 *(1(),y) -> y
 *(x,0()) -> 0()
 *(*(x,y),z) -> *(x,*(y,z))

Proof:
 Bounds Processor:
  bound: 1
  enrichment: match
  automaton:
   final states: {7,6,5,4}
   transitions:
    01() -> 6*,3,4
    11() -> 7*,2,4
    *0(3,1) -> 4*
    *0(3,3) -> 4*
    *0(3,5) -> 4*
    *0(3,7) -> 4*
    *0(5,1) -> 4*
    *0(5,3) -> 4*
    *0(5,5) -> 4*
    *0(5,7) -> 4*
    *0(6,2) -> 4*
    *0(1,2) -> 4*
    *0(6,6) -> 4*
    *0(1,6) -> 4*
    *0(7,1) -> 4*
    *0(2,1) -> 4*
    *0(7,3) -> 4*
    *0(2,3) -> 4*
    *0(7,5) -> 4*
    *0(2,5) -> 4*
    *0(7,7) -> 4*
    *0(2,7) -> 4*
    *0(3,2) -> 4*
    *0(3,6) -> 4*
    *0(5,2) -> 4*
    *0(5,6) -> 4*
    *0(6,1) -> 4*
    *0(1,1) -> 4*
    *0(6,3) -> 4*
    *0(1,3) -> 4*
    *0(6,5) -> 4*
    *0(1,5) -> 4*
    *0(6,7) -> 4*
    *0(1,7) -> 4*
    *0(7,2) -> 4*
    *0(2,2) -> 4*
    *0(7,6) -> 4*
    *0(2,6) -> 4*
    i0(5) -> 4,5*
    i0(7) -> 4,5*
    i0(2) -> 5*,4,1
    i0(6) -> 4,5*
    i0(1) -> 5*,4,1
    i0(3) -> 5*,4,1
    1 -> 4*
    2 -> 4*
    3 -> 4*
    5 -> 4*
    6 -> 4*
    7 -> 4*
  problem:
   
  Qed